body { 
  font-size: 9pt;
  background-color: white;
}

.deprecated {
  color: #ff6666;
}